@$e$($x$$\rightarrow$$v$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$es{-}dtype(${\it es}$; loc($e$); $x$; $T$) c$\wedge$ (($\neg$(es{-}when(${\it es}$; $x$; $e$) = $v$)) $\wedge$ (es{-}after(${\it es}$; $x$; $e$) = $v$))